ds:x:Id fp Type{i}, da:k:Knd fp Type{i}. ecl(ds;da)  Type{i'} 

latex

Definitions	x:A. B(x), t  T, ecl(ds;da), x. t(x), x(s)
Lemmas	Knd wf, decl-state wf, ma-valtype wf, bool wf, nat wf, fpf wf, Id wf